Discussion utilisateur:Simo.93/Brouillon
Première lecture du 03/01/2017 pour la forme - Abdessamad J.[modifier le code]
Bonjour, je suis Abdessamad JARIR, voici quelques points que j'ai pu noter à propos de votre articles premièrement je commence par la forme :
Bonjour Abdessamad J, je suis Lahcene A je suis l'un des rédacteurs de cet article.Je vous remercie pour ces remarques aux quelles j'essayerai de répondre. Cordialement --LahceneTiir (discuter) 6 janvier 2017 à 14:26 (CET)
- dans le résumé introductif j'aurai bien aimé avoir des liens wiki pour la définition des termes suivants : SPIN, ComFoRT.--Abdessamad J (discuter) 3 janvier 2017 à 11:12 (CET)
- le lien de Spin est fait --LahceneTiir (discuter) 6 janvier 2017 à 14:19 (CET)
- par contre il n'ya pas de lien pour ComFoRT --LahceneTiir (discuter) 6 janvier 2017 à 14:19 (CET)
généralité[modifier le code]
définition[modifier le code]
Système d'exploitation[modifier le code]
- Je pense qu'il faut pas laisser operating_system et la traduire en système d'exploitation.--Abdessamad J (discuter) 3 janvier 2017 à 11:16 (CET)
- Ce paragraphe "Prouver formellement ...." et tout les autres paragraphes jusqu’à la section "Outils de vérifications" ne sont pas sourcées.--Abdessamad J (discuter) 3 janvier 2017 à 11:16 (CET)
- Il faut changer OS en SE pour (Système d'exploitation).--Abdessamad J (discuter) 6 janvier 2017 à 14:14 (CET)
- Il est inévitable d’avoir des erreurs dans du code informatique .. => il faut remplacer le "du" en "un", sinon il faut dire sur quel code informatique vous parlez.--Abdessamad J (discuter) 6 janvier 2017 à 14:14 (CET)
- ... par conséquent plus la taille du code est élevé ... => "e" oublié à la fin du élevé.--Abdessamad J (discuter) 6 janvier 2017 à 14:30 (CET)
Méthodes de vérifications[modifier le code]
Model checking[modifier le code]
- Changer le titre Model checking en Vérification de modèles.--Abdessamad J (discuter) 6 janvier 2017 à 14:30 (CET)
- Le model checking ne travail pas => "travailler" mal conjugué, changer en "ne travaille pas" --Abdessamad J (discuter) 6 janvier 2017 à 14:30 (CET)
- une méthode qui pourra être efficasse ... => "efficasse" le mot mal écrit changer en "efficace".--Abdessamad J (discuter) 6 janvier 2017 à 14:30 (CET)
- vu qu'il sont assez volumineux en taille ... => "s" oublié dans "il".--Abdessamad J (discuter) 6 janvier 2017 à 14:39 (CET)
- cela prendrai énormément de temps ... => je pense qu'il faut conjuguer le verbe "prendre" au présent puisque vous parlez sur un fait réel (résulat d'une expérimentation).--Abdessamad J ([[Discussion
utilisateur:Mywiki16|discuter]]) 6 janvier 2017 à 14:50 (CET)
- Le début de ce paragraphe "De plus ... jusqu’à "erreurs" est mal formé + faut utiliser "ce" au lieu de "se" dans "se qui est fait".--Abdessamad J (discuter) 6 janvier 2017 à 14:56 (CET)
- J'aurai aimé avoir un lien wiki vers SLAM!.
theorem proving[modifier le code]
- Manque la deuxième '"' et "de" après le but.--Abdessamad J (discuter) 6 janvier 2017 à 15:02 (CET)
- ... on va en déduire une preuve mathématique et vérifier qu'elle confirme ces propirétés. => faut changer "elle" en "il" puisque vous parlez sur le noyau.Le mot "propirétés" mal écrit changer en "propriétés"--Abdessamad J (discuter) 6 janvier 2017 à 15:15 (CET)
- Manque le majuscule au début de cette phrase "la taille du ...".--Abdessamad J (discuter) 6 janvier 2017 à 15:21 (CET)
- ... cette méthode sur tout types d'OS ... => "s" à la fin de tout au lieu de "t".--Abdessamad J (discuter) 6 janvier 2017 à 15:21 (CET)
- ... en particulier les plus complex ... => manque "es" à la fin de "complex".--Abdessamad J (discuter) 6 janvier 2017 à 15:25 (CET)
- ... la vérification des preuvent mathématiques ... => "preuvent" avec "es" à la fin au lieu de "ent".--Abdessamad J (discuter) 6 janvier 2017 à 15:27 (CET)
- ... cette preuve soit compliqué ... => manque "e" à la fin de "compliqué".--Abdessamad J (discuter) 6 janvier 2017 à 15:29 (CET)
- Cette phrase "A noter que comparer au model checking...mais aussi pourquoi." => je trouve que c'est mal formée.--Abdessamad J (discuter) 6 janvier 2017 à 15:32 (CET)
- Normalement, tout à été corrigé, merci--Loik D./Tiir IIR (discuter) 9 janvier 2017 à 11:31 (CET)
Preuve par le code[modifier le code]
- ... la PCC créé ... => "créé" avec "e" à la fin au lieu de "é".--Abdessamad J (discuter) 6 janvier 2017 à 15:40 (CET)
- ... Ov va trouver deux types de PCC : => je pense vous voulez dire "on" au lieu "ov" :).--Abdessamad J (discuter) 6 janvier 2017 à 15:40 (CET)
Critères communs[modifier le code]
- ... et cela a attisé l’intérêt des chercher ... => l’intérêt des chercheurs vous voulez dire ?--Abdessamad J (discuter) 6 janvier 2017 à 15:44 (CET)
- ... les critères communs sont considéré ... => manque de "s" à la fin de "considéré".--Abdessamad J (discuter) 6 janvier 2017 à 15:48 (CET)
- ... et adhère à un modèle de procès légal. => "adhère" avec "ent" à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 15:48 (CET)
- La phrase "Les critères communs ... comme un standard pour la sécurité informatique" est déjà dite dans le paragraphe précédent.--Abdessamad J (discuter) 6 janvier 2017 à 15:53 (CET)
- Effectivement, corrigé ;-)--Loik D./Tiir IIR (discuter) 9 janvier 2017 à 11:40 (CET)
- ... les standards précédent ... => "précédent" avec "s" à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 15:57 (CET)
- Il vaut mieux avoir un lien vers ces standards ITSEC, TCSEC.--Abdessamad J (discuter) 6 janvier 2017 à 15:57 (CET)
- ... les CC sont plus orienté ... => "orienté" avec "s" à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 16:05 (CET)
- ... les CC sont plus orienté produit et moins orienté procédures que les anciens standards. => "produit" sans "s" et procédures avec "s" ???, soient les deux sans "s" ou avec "s".--Abdessamad (discuter) 6 janvier 2017 à 16:05 (CET)
- ... ils représentent une forte avancé vers la sécurité ... "avancé" avec "s" à la fin.--Mywiki16 (discuter) 6 janvier 2017 à 16:15 (CET)
- ... mais surtout assure ... => "assure" avec "ent" à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 16:15 (CET)
- ... En se qui concerne les noyaux ... => faut utiliser "ce" au lieu de "se".--Abdessamad J (discuter) 6 janvier 2017 à 16:15 (CET)
- ... le nombre de noyau ... le nombre de noyau => "noyau" avec x à la fin.--Abdessamad J (discuter) 6 janvier 2017 à 16:15 (CET)
- Manque des notes pour ITSEC, TCSEC.--Abdessamad J (discuter) 6 janvier 2017 à 17:07 (CET)
- Pour se qui est des fautes d'orthographe, tout à normalement été corrigé.--Loik D./Tiir IIR (discuter) 9 janvier 2017 à 11:40 (CET)
Outils de vérifications[modifier le code]
Langages formels[modifier le code]
- J'aurai aimé avoir un lien wiki vers Langage formel et Haskell. --Abdessamad J (discuter) 6 janvier 2017 à 16:32 (CET)
- Il vaut mieux dire "exécuter un binaire d'application réel," au lieu "exécuter des binaires d'application réels".--Abdessamad J (discuter) 6 janvier 2017 à 16:45 (CET)
- Haskell forme un pont entre les équipes améliorant ... => la phrase n'est pas complète (entre les équipes et quoi?) ou mal formée.--Abdessamad J (discuter) 6 janvier 2017 à 16:45 (CET)
Models checkeur[modifier le code]
- Il vaut mieux je pense comme j'avais signalé le titre "Models checkeur" en français.--Abdessamad J (discuter) 6 janvier 2017 à 16:53 (CET)
- La phrase "Le comportement ... sont Exprimé par TLC." est mal formée avec des erreurs d'orthographe.--Abdessamad J (discuter) 6 janvier 2017 à 16:53 (CET)
Exemple d'OS formellement prouvés[modifier le code]
SeL4[modifier le code]
- Manque d'un lien wiki vers sel4 existe sous le nom Micronoyau L4.--Abdessamad J (discuter) 6 janvier 2017 à 16:58 (CET)
- y'a pas un lien wiki qui pointe vers une page Sel4 par contre on a mis un lien wiki vers la page du micronoyeau L4 même si on préfère ne pas en mettre un car c'est pas bien expliqué , c'est pour cela on amis une référence plus détaillé vers un document qui parle du Sel4--Simo.93 (discuter) 8 janvier 2017 à 14:24 (CET)
Intérêts de la vérification formelle d'OS[modifier le code]
Sécurité[modifier le code]
- Je pense qu'il faut faire une note pour expliquer c'est quoi l'approche MILS ?.--Abdessamad J (discuter) 6 janvier 2017 à 17:05 (CET)
- De préférence avoir un lien wiki vers hyperviseur.--Abdessamad J (discuter) 6 janvier 2017 à 17:05 (CET)
- Cette phrase n'est pas claire et mal formée "ainsi que les systèmes qui exigent l'utilisation de langages de type sécurisé Tous les codes".--Abdessamad J (discuter) 6 janvier 2017 à 17:19 (CET)
- il y avait une petite erreur de virgule --Narjis.taou (discuter) 8 janvier 2017 à 15:07 (CET)
- Cette phrase "Ceci peut être ... par le programmeur." est confuse, peut être vaut mieux de la reformuler pour mieux comprendre l'idée.--Abdessamad J (discuter) 6 janvier 2017 à 17:19 (CET)
- phrase relu merci de ta contribution --Narjis.taou (discuter) 8 janvier 2017 à 15:09 (CET)
- En tant que tel => je pense manque "le" dans tel puisque vous parlez sur sel4 que vous avez désigné comme une plateforme.--
- le mot en tant que tel remplace Sel4 donc pas la peine de le cité à nouveau --Narjis.taou (discuter) 8 janvier 2017 à 15:10 (CET)
Abdessamad J (discuter) 6 janvier 2017 à 17:24 (CET)
- ... qui permettra la construction de systèmes ... => de préférence conjuguer le verbe "permettre" au présent.--
- fait --Narjis.taou (discuter) 8 janvier 2017 à 15:12 (CET)Abdessamad J (discuter) 6 janvier 2017 à 17:24 (CET)
- ... tels que l'exécution sûre ... => je pense "tels" doit être "telle" (une exécution).--Abdessamad J (discuter) 6 janvier 2017 à 17:29 (CET)
- ... La technique utilisé pour la vérification => manque "e" dans "utilisé".--Abdessamad J (discuter) 6 janvier 2017 à 17:29 (CET)
- Le paragraphe qui commence par "La technique utilisée" n'est pas clair et mal formé avec des erreurs d'orthographes.--Abdessamad J (discuter) 6 janvier 2017 à 17:39 (CET)
- paragraphe relu merci de ta contribution --Narjis.taou (discuter) 8 janvier 2017 à 15:02 (CET)
Coûts[modifier le code]
- Je pense qu'il vaut mieux faire des notes pour ACL2, Coq, PVS, HOL.--Abdessamad J (discuter) 6 janvier 2017 à 17:56 (CET)
- il y a des phrases mal formulées et incompréhensibles comme La phrase "Des assistants ... réussies"--Abdessamad J (discuter) 6 janvier 2017 à 17:56 (CET)
Historique[modifier le code]
- Je pense que ce n'est pas la peine de mettre ?, soit on connaît la date on la met sinon on ne met pas, l’essentiel il faut préciser.--Abdessamad J (discuter) 6 janvier 2017 à 17:56 (CET)
- Je pense qu'il faut tout de même le mettre. Car même si on ne connait pas la date (de début ou de fin), on a au moins une idée de la période pendant laquelle c'est déroulé le projet.--Loik D./Tiir IIR (discuter) --Tiir IIR (discuter)--Tiir IIR (discuter)--Tiir IIR (discuter)--Tiir IIR (discuter) 11 janvier 2017 à 10:41 (CET)
Note[modifier le code]
- De préférence avoir une section pour les notes
Deuxième lecture du 06/01/2017 pour le Fond - Abdessamad J.[modifier le code]
Bonjour, je me permet de vous relire pour une deuxième fois pour faire des remarques sur le fond de vos articles :
Bonjour je vous remercie pour ces remarques aux quelles on va essayer de vous répondre. Cordialement --LahceneTiir (discuter) 8 janvier 2017 à 06:54 (CET)
Généralités[modifier le code]
Définitions[modifier le code]
Système d'exploitation[modifier le code]
- Vous avez dit n’importe quel code informatique, peut être convertit mathématiquement, mais vous n'avez pas donnée un exemple.--Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)
- On a bien donné un exemple de micronoyau seL4.--LahceneTiir (discuter) 8 janvier 2017 à 06:49 (CET)
Méthodes de vérifications[modifier le code]
- Dans cette partie je trouve que vous avez parlé sur ces méthodes sans prouver leur efficacité.(montrer des recherches, des résultats qui ont étés faites sur l'efficacité de ces méthodes) --Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)
- le but de cette partie c'est de citer quelques méthodes, et pas rentré dans les détails car cela est un autre sujet à Aborder --Narjis.taou (discuter) 8 janvier 2017 à 20:51 (CET)
Preuve par le code[modifier le code]
- Ici vous avez juste mentionner les frameworks type PCC conventionnel, PCC fondationel sans parler sur la particularité de chaque type et comment ils peuvent vérifient une preuve mathématique ?--Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)
- Vous avez cité un point négatif sur cette méthode sans dire s'il y a des points positifs ou non si oui il faut les dire comme vous avez mentionné le point négatif.--Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)
Critères communs[modifier le code]
- Vous critiquez les méthodes formelles avant de montrer leurs intérêts, je pense qu'il faut faire l'inverse.--Abdessamad J (discuter) 6 janvier 2017 à 18:46 (CET)
- Effectivement, j'ai modifié cela.--Loik D./Tiir IIR (discuter) 10 janvier 2017 à 14:13 (CET)
Remarque générale[modifier le code]
Je pense que le sujet manque des points importants comme :
- de montrer l’intérêt des systèmes formellement prouvés.--Abdessamad J (discuter) 6 janvier 2017 à 19:17 (CET)
- de dire s'il y a des risques pendant la vérification formelle du système--Abdessamad J (discuter) 6 janvier 2017 à 19:01 (CET)
- veuillez lire s'il vous plait la partie critères communs. Merci --Narjis.taou (discuter) 8 janvier 2017 à 21:17 (CET)
- oui je l'ai déjà bien lu moi je parle sur l’intérêt de prouver les systèmes même dans la vie de l'entreprise, et non pas l’intérêt de la vérification des systèmes.--Abdessamad J (discuter) 11 janvier 2017 à 10:52 (CET)